FairFifo
== (i:Id, t:, l:IdLnk. source(l) = i  onlnk(l;m(i;t)) = nil)
== & (i:Id, t:. isnull(a(i;t))  (x:Id. s(i;t+1).x = s(i;t).x) & m(i;t) = nil)
== & (i:Id, t:, l:IdLnk.
== & (isrcv(l;a(i;t))  destination(l) = i & ||queue(l;t)||1 & hd(queue(l;t)) = msg(a(i;t)))
== & & (l:IdLnk, t:. t':. tt' & isrcv(l;a(destination(l);t'))  queue(l;t') = nil)
== & & & w-machine-constraint(w)
== & & & w-atom-constraint(w) 

latex

---

clarification:

fair-fifo{i:l}
fair-fifo(w)
== (i:Id, t:, l:IdLnk. source(l) = i  Id  onlnk(l;w-m(w; i; t)) = nil  w-Msg(w) List)
== & (i:Id, t:.
== & (w-isnull(w; w-a(w; i; t))
== & ( (x:Id. w-s(w; i; (t+1); x) = w-s(w; i; t; x)  w-vartype(w; i; x))
== & ( & w-m(w; i; t) = nil  w-Msg(w) List)
== & (i:Id, t:, l:IdLnk.
== & (w-isrcvl(w; l; w-a(w; i; t))
== & ( destination(l) = i  Id
== & ( & ||w-queue(w; l; t)||1 & hd(w-queue(w; l; t)) = w-msg(w; w-a(w; i; t))  w-Msg(w))
== & & (l:IdLnk, t:.
== & & (t':.
== & & (tt' & w-isrcvl(w; l; w-a(w; destination(l); t'))  w-queue(w; l; t') = nil  w-Msg(w) List)
== & & & w-machine-constraint(w)
== & & & w-atom-constraint{i:l}
== & & & w-atom-constraint(w) 

latex

Definitions	A, source(l), onlnk(l;mss), isnull(a), vartype(i;x), n+m, s(i;t).x, m(i;t), P  Q, Id, A & B, ij, ||as||, #$n, hd(l), msg(a), IdLnk, x:A. B(x), x:A. B(x), , AB, P  Q, b, isrcv(l;a), a(i;t), destination(l), s = t, type List, Msg, queue(l;t), nil, P & Q, w-machine-constraint(w), w-atom-constraint(w)
FDL editor aliases	fair-fifo